perm filename DOC[EKL,SYS] blob
sn#860108 filedate 1988-08-18 generic text, type C, neo UTF8
COMMENT ⊗ VALID 00008 PAGES
C REC PAGE DESCRIPTION
C00001 00001
C00002 00002 Facts about reverse:
C00004 00003 A proof of Ramsey's Theorem
C00005 00004 The pigeon hole principle and proofs that permutations are a group
C00009 00005 general facts about maps in the category of sets
C00012 00006 A problem in non monotonic reasoning
C00013 00007 The quantifier `there exists exactly one'
C00014 00008 The Landau project
C00016 ENDMK
C⊗;
;Facts about reverse:
;File names:
;natnum[ekl,sys] ;facts of natural numbers, involving <,',+ and *
;lispax[ekl,sys] ;axioms of LISP
;reverse[ekl,sys] ;facts about reverse
;lthrev[ekl,sys] ;facts about length and reverse
;Facts about reverse are given in the following order
; lispax
; |
; ↓
; reverse natnum
; | |
; |_________________|
; |
; ↓
; lthrev
;A proof of Ramsey's Theorem
;File names:
;natnum[ekl,sys] ;facts of natural numbers, involving <,',+ and *
;natset[ekl,sys] ;facts of set theory
;ramsey[ekl,sys] ;proof of the theorem
;File organization:
; natnum
; ↓
; natset
; ↓
; ramsey
;The functional interpretation of Infinite Ramsey
;This is a fragment, i.e. the base case in the main induction.
; ramsey.nci
;The pigeon hole principle and proofs that permutations are a group
;(see the paper G.Bellin and J.Ketonen, Experiments in Authomatic Theorem Proving)
;which explains the material.
;File names:
;normal[ekl,sys] ;a normalizer of (propositional) expressions
;natnum[ekl,sys] ;facts of natural numbers, involving <,',+ and *
;minus[ekl,sys] ;facts of natural numbers, involving ≤ and -
;lispax[ekl,sys] ;axioms of LISP
;allp[ekl,sys] ;facts about the bounded quantifier allp
;set[ekl,sys] ;rudiments of set theory
;length[ekl,sys] ;length of lists
;nth[ekl,sys] ;the nth function and its relatives
;appl[ekl,sys] ;two notions of application, via lists of numbers
;sums[ekl,sys] ;finite sums and unions
;mult[ekl,sys] ;multiplicity and their properties
;pigeon[ekl,sys] ;the prigeon hole principle in 2nd order arithmetic
;alpig[ekl,sys] ;application of the pigeon hole to alists
;invima[ekl,sys]; ;a generalization (third application)
;assoc[ekl,sys] ;permutations are a group (using alists)
;lpig[ekl,sys] ;application of the pigeon hole to lists of numbers
;permp[ekl,sys] ;permutations are a group (lists, using predicates)
;permf[ekl,sys] ;permutations are a group (lists, using functions)
;File organization:
; natnum normal lispax
; | | ↓
; |____________| allp ;fix somepfacts
; ↓ ↓
; minus set
; |___________________________|
; ↓
; length
; ↓
; nth
; ↓
; appl
; _____________|______________________
; ↓ ↓ ↓ ↓
; sums assoc permp permf
; ↓
; mult
; ↓
; pigeon
; _____________
; ↓ ↓
; alpig lpig
; ↓
; invima
;general facts about maps in the category of sets
;catset.gen[ekl,sys]
;A problem in non monotonic reasoning
;bird[ekl,sys] ;most birds can fly, but not all:
; ;use of the predicate `ab' (abnormal)
;The quantifier `there exists exactly one'
;unique[ekl,sys] ;∃!
;The Landau project
;formalizing ``Foundations of Analysis'' by E.Landau, Chelsea NY 1951
;the following files contain the formalization of the first 50 pages
;nat.lan[ekl,sys] ;natural numbers
;frac.lan[ekl,sys] ;fractions
;rat.lan[ekl,sys] ;rational numbers
;cut.lan[ekl,sys] ;Dedekind cuts
;File organization:
; nat.lan lispax[ekl,sys]
; | |
; |_________________________|
; |
; ↓
; frac.lan
; |
; ↓
; rat.lan
; |
; ↓
; cut.lan